fix: Add missing type characteristics #154
Conversation
This reverts commit ce5c491.
src/Collections/Sequences/Seq.dfy
Outdated
| @@ -653,7 +653,7 @@ module {:options "-functionSyntax:4"} Seq { | |||
| /* Applying a function to a sequence is distributive over concatenation. That is, concatenating | |||
| two sequences and then applying Map is the same as applying Map to each sequence separately, | |||
| and then concatenating the two resulting sequences. */ | |||
| lemma {:opaque} LemmaMapDistributesOverConcat<T,R>(f: (T ~> R), xs: seq<T>, ys: seq<T>) | |||
| lemma {:opaque} LemmaMapDistributesOverConcat<T, R>(f: (T ~> R), xs: seq<T>, ys: seq<T>) | |||
There was a problem hiding this comment.
Thanks, that makes no sense. I removed them. I also removed them in dafny-lang/dafny#4928.
| @@ -15,7 +15,7 @@ module Dafny.Collections.Arrays { | |||
| import opened Relations | |||
| import opened Seq | |||
|
|
|||
| method BinarySearch<T>(a: array<T>, key: T, less: (T, T) -> bool) returns (r: Option<nat>) | |||
| method BinarySearch<T(!new)>(a: array<T>, key: T, less: (T, T) -> bool) returns (r: Option<nat>) | |||
There was a problem hiding this comment.
I'm very surprised by this type characteristic. I would have thought it would have been possible to sort an array of arrays by the size of each array for example. Why is this required now? Can we relax it if possible?
There was a problem hiding this comment.
It's because of how the specification was written. The precondition uses StrictTotalOrdering, which ends up quantifying over all values of the type. If those ordering predicates were instead written to apply only to an element of given set or sequence, then the (!new) would not be needed.
There was a problem hiding this comment.
When I wrote my last message, I hadn't seen yours on the thread. I should have refreshed the page first.
|
Note, this |
This PR primarily adds missing
(!new)type characteristics in function declarations. These had gone undetected, because of a latent bug that has now been fixed. The bug fix requires these fixes in the libraries.This PR also cleans up some library files: removing deprecated semi-colons, removing unnecessary parentheses, stylizing order of specification clauses, and removing explicit triggers that are saying the same thing as those triggers that are automatically inferred.
The PR also changesforall ensures ...statements with no bound variables intoassert ... bystatements. (I think we attempted this change once before, only to find that the change tickled some brittleness issue. Let's see if they verify this time.)Finally, the PR improves some
reads fnclauses, wherefnis some function. In one case, such areadsclause was probably accidentally (and I changed it to the more specificreads fn(this)). In the other cases, thereads fnclause had ended up reading more than the enclosing function's precondition could support. The newreadsclauses are more specific than the previous, so, semantically, they should not affect callers. I'm surprised how these were not detected before (am I perhaps running the wrong version of Dafny when running thelibrariestest suite?). In fact, I also received an error, which I think is due to that a previous version of Dafny didn't assumerequiresclauses when checkingreadsclauses in lambda expressions (or was it perhaps the other way around?). If there's still a problem with my modifications, I hope CI will discover them.Hint to reviewers: If you want to see each of the simple modifications, I suggest looking at each commit individually.
By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.